package flowlogic;

import java.util.ArrayList;
import java.util.HashMap;
import java.util.HashSet;

import ast.Assert;
import ast.Binder;
import ast.CompositeBinder;
import ast.In;
import ast.Out;
import ast.Term;

public class BinderJudgement extends FLJudgement {

	private Binder binder;
	private PsiNode psi;
	
	public BinderJudgement(Binder bd, HashMap<String, HashSet<Term>> rho)
	{
		binder = bd;
		setRho(rho);
		psi = new PsiNode();
	}
	
	public PsiNode getPsi()
	{
		return psi;
	}
	
	public String toString()
	{
		String res = "";
		res += "rho" + " |- " + binder + " : " + psi;
		return res;
	}
	
	public ArrayList<DischargeResult> discharge()
	{
		ArrayList<DischargeResult> res = new ArrayList<DischargeResult>();
		
		HashSet<Node> vals1 = new HashSet<Node>();
		vals1.add(SrtSignal.getInstance());
		
		if (binder instanceof Out) {
			
			TermJudgement tj = new TermJudgement(((Out) binder).getT(), getRho());	
			PsiNode psiT = tj.getPsi();
			ResNode resT = tj.getRes();
			TermJudgement tj1 = new TermJudgement(((Out) binder).getT1(), getRho());
			ResNode resT1 = tj1.getRes();
			res.add(tj);
			res.add(tj1);
			
			res.add(new Inclusion(psiT, psi, true));
			res.add(new Inclusion(tj1.getPsi(), psi, true));
			
			BoundVariable bv1 = new BoundVariable("#tc");
			HashSet<Node> t1Set = new HashSet<Node>();
			t1Set.add(new FreeVariable("#v1"));
			Inclusion incl1 = new Inclusion(
								new ConcreteSetNode(t1Set),
								new KappaNode(new FreeVariable("#tc")), true
							  );
			ForallConstraint inner = new ForallConstraint(
								new BoundVariable("#v1"),
								resT1,
								incl1);
			ForallConstraint forall1 = new ForallConstraint(bv1, resT, inner);
			res.add(forall1);
			
		} else if (binder instanceof In) {
			
			TermJudgement tj = new TermJudgement(((In) binder).getT(), getRho());	
			PsiNode psiT = tj.getPsi();
			res.add(tj);
			res.add(new Inclusion(psiT, psi, true));
			
			FreeVariable fv = new FreeVariable("#tc");
			HashSet<Term> extDataSingleton = new HashSet<Term>();
			extDataSingleton.add(ExternalData.getInstance());
			String binderBvName = ((In) binder).getX().getName();
			GuardedConstraint cs1 = new GuardedConstraint(
						new ExtNode(fv), 
						new Inclusion(new ResNode(extDataSingleton),
								      new RhoNode(new FreeVariable(binderBvName)), true));
			BoundVariable bv1 = new BoundVariable("#tc");
			res.add(new ForallConstraint(bv1, tj.getRes(), cs1));
			GuardedConstraint cs2 = new GuardedConstraint(
						new IntNode(fv),
						new Inclusion(new KappaNode(fv),
									  new RhoNode(new FreeVariable(binderBvName)), true));
			res.add(new ForallConstraint(bv1, tj.getRes(), cs2));
			
		} else if (binder instanceof CompositeBinder) {
			
			ArrayList<Binder> componentBinders = 
					((CompositeBinder) binder).getComponentBinders();
			for (Binder cmpBd : componentBinders) {
				BinderJudgement bdjgt = new BinderJudgement(cmpBd, getRho());
				res.add(bdjgt);
				res.add(new Inclusion(bdjgt.getPsi(), psi, true));
			}
			
		} else {
			assert (binder instanceof Assert);
			res.add(new BinderJudgement(((Assert) binder).getBinder(), getRho()));
		}
		
		return res;
	}
	
}
